Nuprl Lemma : bnot_of_le_int
12,41
postcript
pdf
i
,
j
:
. (
i
z
j
) =
j
<z
i
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
i
z
j
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
bnot
bnot
elim
,
lt
int
wf
,
bool
wf
origin
i, j:
. (
i 
z j) = j <z i 
i, j:. (i z j) = j <z i
Tx:A. B(x)z j
Q
Q Q